<html>
<head><meta charset="utf-8"><title>Inconsistency in MIR for branches · wg-formal-methods · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/index.html">wg-formal-methods</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Inconsistency.20in.20MIR.20for.20branches.html">Inconsistency in MIR for branches</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="214769775"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Inconsistency%20in%20MIR%20for%20branches/near/214769775" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Inconsistency.20in.20MIR.20for.20branches.html#214769775">(Oct 27 2020 at 21:58)</a>:</h4>
<p>This isn't a correctness issue, but i noticed something odd in the MIR for several branches, if you move into a borrow in a branch, all but one branch will be compiled to a reborrow. It's probably not clear when I say it like this but it should be with MIR:</p>
<p>Given the rust code:</p>
<div class="codehilite"><pre><span></span><code>fn main () {
  let mut a = 10;
  let mut b = 10;
  let mut c = 10;

  let x = &amp;mut a;
  let y = &amp;mut b;
  let z = &amp;mut c;
  let mut w;


  match 3 {
    1 =&gt; { * x = 6; w = x; }
    2 =&gt; { * y = 7; w = y; }
    _ =&gt; { * z = 8; w = z; }
  }

  * w = 5;
}
</code></pre></div>


<p>We get the MIR: (annotated with polonius loan liveness)</p>
<div class="codehilite"><pre><span></span><code>StorageLive(_1)                     live=[L5, L6] dying=[]
_1 = const 10_i32                   live=[L5, L6] dying=[]
FakeRead(ForLet, _1)                live=[L5, L6] dying=[]
StorageLive(_2)                     live=[L5, L6] dying=[]
_2 = const 10_i32                   live=[L5, L6] dying=[]
FakeRead(ForLet, _2)                live=[L5, L6] dying=[]
StorageLive(_3)                     live=[L5, L6] dying=[]
_3 = const 10_i32                   live=[L5, L6] dying=[]
FakeRead(ForLet, _3)                live=[L5, L6] dying=[]
StorageLive(_4)                     live=[L5, L6] dying=[]
_4 = &amp;mut _1                        live=[L5, L6] dying=[]
FakeRead(ForLet, _4)                live=[L0, L5, L6] dying=[]
StorageLive(_5)                     live=[L0, L5, L6] dying=[]
_5 = &amp;mut _2                        live=[L0, L5, L6] dying=[]
FakeRead(ForLet, _5)                live=[L0, L1, L5, L6] dying=[]
StorageLive(_6)                     live=[L0, L1, L5, L6] dying=[]
_6 = &amp;mut _3                        live=[L0, L1, L5, L6] dying=[]
FakeRead(ForLet, _6)                live=[L0, L1, L2, L5, L6] dying=[]
StorageLive(_7)                     live=[L0, L1, L2, L5, L6] dying=[]
StorageLive(_8)                     live=[L0, L1, L2, L5, L6] dying=[]
StorageLive(_9)                     live=[L0, L1, L2, L5, L6] dying=[]
_9 = const 3_i32                    live=[L0, L1, L2, L5, L6] dying=[]
FakeRead(ForMatchedPlace, _9)       live=[L0, L1, L2, L5, L6] dying=[]
switchInt(_9) -&gt; [1_i32: bb1, 2_i32: bb2, otherwise: bb3] live=[L0, L1, L2, L5, L6] dying=[]

falseEdge -&gt; [real: bb4, imaginary: bb2] live=[L0, L1, L2, L5, L6] dying=[]

falseEdge -&gt; [real: bb5, imaginary: bb3] live=[L1, L2, L5, L6] dying=[]

(*_6) = const 8_i32                 live=[L2, L5, L6] dying=[]
StorageLive(_12)                    live=[L2, L5, L6] dying=[]
_12 = &amp;mut (*_6)                    live=[L2, L5, L6] dying=[]
_7 = move _12                       live=[L2, L3, L5, L6] dying=[]
StorageDead(_12)                    live=[L2, L3, L5, L6] dying=[]
_8 = const ()                       live=[L2, L3, L5, L6] dying=[]
goto -&gt; bb6                         live=[L2, L3, L5, L6] dying=[]

(*_4) = const 6_i32                 live=[L0, L5, L6] dying=[]
StorageLive(_10)                    live=[L0, L5, L6] dying=[]
_10 = move _4                       live=[L0, L5, L6] dying=[]
_7 = move _10                       live=[L0, L5, L6] dying=[]
StorageDead(_10)                    live=[L0, L5, L6] dying=[]
_8 = const ()                       live=[L0, L5, L6] dying=[]
goto -&gt; bb6                         live=[L0, L5, L6] dying=[]

(*_5) = const 7_i32                 live=[L1, L5, L6] dying=[]
StorageLive(_11)                    live=[L1, L5, L6] dying=[]
_11 = &amp;mut (*_5)                    live=[L1, L5, L6] dying=[]
_7 = move _11                       live=[L1, L4, L5, L6] dying=[]
StorageDead(_11)                    live=[L1, L4, L5, L6] dying=[]
_8 = const ()                       live=[L1, L4, L5, L6] dying=[]
goto -&gt; bb6                         live=[L1, L4, L5, L6] dying=[]

StorageDead(_9)                     live=[L0, L1, L2, L3, L4, L5, L6] dying=[]
StorageDead(_8)                     live=[L0, L1, L2, L3, L4, L5, L6] dying=[]
(*_7) = const 5_i32                 live=[L0, L1, L2, L3, L4, L5, L6] dying=[L0, L1, L2, L3, L4]
_0 = const ()                       live=[L5, L6] dying=[]
StorageDead(_7)                     live=[L5, L6] dying=[]
StorageDead(_6)                     live=[L5, L6] dying=[]
StorageDead(_5)                     live=[L5, L6] dying=[]
StorageDead(_4)                     live=[L5, L6] dying=[]
StorageDead(_3)                     live=[L5, L6] dying=[]
StorageDead(_2)                     live=[L5, L6] dying=[]
StorageDead(_1)                     live=[L5, L6] dying=[]
return                              live=[L5, L6] dying=[L5, L6]
</code></pre></div>


<p>Note how _4 is not reborrowed before assigning into _10.<br>
Is there any reason  for this I'm missing? or is it just an implementation artefact?</p>



<a name="214802666"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Inconsistency%20in%20MIR%20for%20branches/near/214802666" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Inconsistency.20in.20MIR.20for.20branches.html#214802666">(Oct 28 2020 at 07:31)</a>:</h4>
<p>I guess you are more likely to get an explanation in <a class="stream" data-stream-id="186049" href="/#narrow/stream/186049-t-compiler.2Fwg-polonius">#t-compiler/wg-polonius</a>.</p>



<a name="214817899"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Inconsistency%20in%20MIR%20for%20branches/near/214817899" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Inconsistency.20in.20MIR.20for.20branches.html#214817899">(Oct 28 2020 at 10:31)</a>:</h4>
<p>Yea I wasn't really sure since this seems like it's more of a compilation question</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>